public class Unifier {
    Stack<Variable> bound;
    
    public boolean unify(Term x, Term y) {
        bound = null;
        
        if(unify_loop(x,y)) {
            return true;
        }
        else {
            unbind();
            return false;
        }
    }
    
    public void bind(Term variable, Term value) {
        if(variable == value) {
            System.out.println("!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
        }
        else {
            bound = new Stack<Variable>((Variable)variable,bound);
            ((Variable)variable).bind(value);
        }
    }
    
    public void unbind() {
        while(bound != null) {
            bound.head.unbind();
            bound = bound.tail;
        }
    }
    
    public boolean unify_loop(Term x, Term y) {
        x = x.deref();
        y = y.deref();
        
        if(x.kind == Term.Kind.VARIABLE) {
            if(y.kind == Term.Kind.VARIABLE) {
                bind(x,y);
                return true;
            }
            else if(y.kind == Term.Kind.COMPOUND) {
                if(((Compound)y).contains(x)) {
                    return false;
                }
                else {
                    bind(x,y);
                    return true;
                }
            }
        }
        else if(x.kind == Term.Kind.COMPOUND) {
            if(y.kind == Term.Kind.VARIABLE) {
                if(((Compound)x).contains(y)) {
                    return false;
                }
                else {
                    bind(y,x);
                    return true;
                }
            }
            else if(y.kind == Term.Kind.COMPOUND) {
                Compound xc = (Compound)x;
                Compound yc = (Compound)y;
                
                if(xc.arity == yc.arity && xc.name.equals(yc.name)) {
                    for(int i = 0; i < xc.arity; i++) {
                        if(!unify_loop(xc.args[i],yc.args[i])) {
                            return false;
                        }
                    }
                    return true;
                }
                else {
                    return false;
                }
            }
        }
        
        return false;
    }
}
